w-machine-constraint(w)
== i:Id.
== let Choose,Trans,Send = w-machine(w;i) in 
== t:.
== isnull(a(i;t))
==  (x.s(i;t+1).x) = Trans(kind(a(i;t)),val(a(i;t)),x.s(i;t).x)
==  & (islocal(kind(a(i;t)))
==  & ( isl(Choose(act(kind(a(i;t))),x.s(i;t).x))
==  & ( & val(a(i;t)) = outl(Choose(act(kind(a(i;t))),x.s(i;t).x)))
==  & m(i;t) = Send(kind(a(i;t)),val(a(i;t)),x.s(i;t).x) 

latex

---

clarification:

w-machine-constraint(w)
== i:Id.
== let Choose,Trans,Send = w-machine(w;i) in 
== t:.
== w-isnull(w; w-a(w; i; t))
==  (x.w-s(w; i; (t+1); x))
==  =
==  Trans(w-kind(w; w-a(w; i; t)),w-val(w; w-a(w; i; t)),x.w-s(w; i; t; x))
==   x:Idw-vartype(w; i; x)
==  & (islocal(w-kind(w; w-a(w; i; t)))
==  & ( isl(Choose(act(w-kind(w; w-a(w; i; t))),x.w-s(w; i; t; x)))
==  & ( & w-val(w; w-a(w; i; t))
==  & ( & =
==  & ( & outl(Choose(act(w-kind(w; w-a(w; i; t))),x.w-s(w; i; t; x)))
==  & ( &  w-valtype(w; i; w-a(w; i; t)))
==  & w-m(w; i; t)
==  & =
==  & Send(w-kind(w; w-a(w; i; t)),w-val(w; w-a(w; i; t)),x.w-s(w; i; t; x))
==  &  Msg(w.M) List 

latex

Definitions	let x,y,z = a in t(x;y;z), w-machine(w;i), x:A. B(x), , A, isnull(a), x:AB(x), Id, vartype(i;x), n+m, #$n, P & Q, P  Q, islocal(k), A & B, b, isl(x), valtype(i;a), outl(x), act(k), s = t, type List, Msg(M), w.M, m(i;t), f(a), kind(a), val(a), a(i;t), x.A(x), s(i;t).x
FDL editor aliases	w-machine-constraint